/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.SortedSet;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.LeafId;
import alloy.subscope.ExprRelationInfo;
import alloy.subscope.RelAnnotation;
import alloy.subscope.ScopedSigsInfo;
import alloy.transl.ASTInfo;
import alloy.transl.ExprTransl;
import alloy.transl.RelationAllocator;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.util.Dbg;
import alloy.util.IntRange;
import alloy.util.MultiDimIter;
import alloy.util.Util;

/**
 * Symmetry-breaking method that uses subscope information to allocate
 * specific subranges of atoms of a basic type to specific scoped sigs.
 * For example, if we have declarations such as
 * <pre>
 * sig A  { }
 * sig B extends A { }
 * </pre>
 * and run a command for 4 A, 2 B, then since we know that at most two
 * atoms of A belong to B, we can restrict B to two particular atoms of
 * A, say A_0 and A_1.  Then if we have a relation r: B->C, then even
 * though the {@link RelationType} of this relation is A->A,
 * we know it cannot contain any tuples of the form <A_2,...> or <A_3,...>,
 * so we can force Boolean variables allocated to these tuples to FALSE.
 * <p>
 * Another way to look at it is, given an instance, we can always swap
 * the atoms of A to obtain an isomorphic instance in which B is restricted
 * to the two particular atoms we have chosen.
 *
 * @see alloy.subscope
 */
class SBM_Subscopes extends SymmetryBreakingMethod {
    /** Information about the "tree" of scoped sigs */
    private ScopedSigsInfo _sigsInfo;
    
    /**
     * {@link Map} from {@link LeafId} of a scoped sig to the scope set for it,
     * if a scope was set for it.  Same as {@link alloy.ast.Command#leafId2scope}.
     */
    private Map /* LeafId->Integer */ _leafId2scope;

    /**
     * Relation annotations that can tell us that certain
     * tuples can never be in a relation.
     * @see alloy.subscope
     */
    private Map /* LeafId->ExprRelationInfo */ _id2Annotation;

    private static final boolean dbg = false;

    //////////////
    // Methods //
    ////////////

    SBM_Subscopes(ASTInfo astInfo_,
		  RelationAllocator relAlloc_,
		  ScopedSigsInfo sigsInfo_,
		  Map /* LeafId->Integer */ leafId2scope_,
		  Map /* LeafId->ExprRelationInfo */ id2Annotation_) {
	super(astInfo_, relAlloc_);
	_sigsInfo = sigsInfo_;
	_leafId2scope = leafId2scope_;
	_id2Annotation = id2Annotation_;
    }
    
    /**
     * Break symmetry using subscopes for the given {@link BasicType},
     * and update the available symmetry information accordingly.
     */
    SymmetryBreakingPredicate breakSymmetry(AvailableSymmetry availSymm_,
					    Set /* of BasicType */ basicTypes_) {
	// For breaking symmetries using subscopes, we can only use basic types
	// all of whose atoms are completely interchangeable -- i.e. basic types
	// on which no symmetry has been broken yet.  Let's make a list of these.
	Set /* of BasicType */ symmBasicTypes = new TreeSet();
	for (Iterator btypeIter = basicTypes_.iterator(); btypeIter.hasNext();) {
	    BasicType btype = (BasicType)btypeIter.next();
	    if (btype instanceof SigType &&  // if it's not an IntType...
		availSymm_.isFullySymmetric(btype))
		symmBasicTypes.add(btype);
	}
	if (symmBasicTypes.isEmpty()) return new SymmetryBreakingPredicate();
	
	/**
	 * First, we build a Map from LeafId of each scoped sig
	 * that is a subsignature of one of basicTypes_
	 * to an IntRange giving the range of atoms of the basic type
	 * assigned to the scoped sig.
	 */
	Map /* LeafId->IntRange */ sigId2atomRange = new TreeMap();

	_allocateAtomRanges(symmBasicTypes, sigId2atomRange);
	_updateAvailableSymmetry(symmBasicTypes, sigId2atomRange, availSymm_);
	return _constructPredicate(symmBasicTypes, sigId2atomRange);


    }  // SBM_Subscopes()

    /** Allocate atom ranges to scoped sigs. */
    private void  _allocateAtomRanges(Set /* of BasicType */ symmBasicTypes_,
				      Map /* LeafId->IntRange */ sigId2atomRange_) {
	for (Iterator relIter = _astInfo.getRelations().iterator(); relIter.hasNext();) {
	    LeafId relId = (LeafId)relIter.next();
	    RelationType relType = _astInfo.getLeafType(relId);
	    BasicType sigBasicType = relType.getBasicTypeAt(0);
	    if (relType.numBasicTypes() == 1 &&
		symmBasicTypes_.contains(sigBasicType) &&
		_sigsInfo.isScopedSig(relId) &&
		_sigsInfo.parentSigId(relId) == null) {
		// So, this relId is the LeafId for a SigExpr representing the set
		// of all atoms of a BasicType.  We assign the full range of atoms
		// to this set, then call _allocateScopedSigAtoms() to recursively
		// partition this range of atoms among any scoped sig children.
		_recordAtomRange(relId, 0, sigBasicType.getScope(), sigId2atomRange_);
	    }  // if this LeafId is for a SigExpr of a BasicType...
	}  // loop over all relations
    }  // _allocateAtomRanges()

    /** Update "available symmetry" information */
    private void _updateAvailableSymmetry(Set /* of BasicType */ symmBasicTypes_,
					  Map /* LeafId->IntRange */ sigId2atomRange_,
					  AvailableSymmetry availSymm_) {
	// Record the modifications to "available symmetry" information
	
	// Build a map from BasicType to the set of dividers i.e. ends of IntRanges
	// of atoms on that basic type
	Map /* BasicType->SortedSet[Integer] */ btype2Dividers = new TreeMap();
	for (Iterator entryIter = sigId2atomRange_.entrySet().iterator(); entryIter.hasNext();) {
	    Map.Entry entry = (Map.Entry)entryIter.next();
	    LeafId sigId = (LeafId)entry.getKey();
	    IntRange atomRange = (IntRange)entry.getValue();
	    BasicType btype = _astInfo.getLeafType(sigId).getBasicTypeAt(0);
	    SortedSet /* of Integer */ dividers = (SortedSet)btype2Dividers.get(btype);
	    if (dividers == null)
		btype2Dividers.put(btype, dividers = new TreeSet());
	    dividers.add(new Integer(atomRange.to));
	}
	
	for (Iterator basicTypeIter = symmBasicTypes_.iterator(); basicTypeIter.hasNext();) {
	    BasicType btype = (BasicType)basicTypeIter.next();
	    availSymm_.removeAllSymmetry(btype);  // ok because these types had full symmetry to start with
	    SortedSet /* of Integer */ dividers = (SortedSet)btype2Dividers.get(btype);
	    int rangeStart = 0;
	    for (Iterator divIter = dividers.iterator(); divIter.hasNext();) {
		Integer div = (Integer)divIter.next();
		availSymm_.addSymmSet(btype, new AtomSet(rangeStart, div.intValue()));
		rangeStart = div.intValue();
	    }
	}
    }  // _updateAvailableSymmetry()

    /**
     * Construct the symmetry-breaking predicate which zeroes out those tuples that cannot be present.
     */
    private SymmetryBreakingPredicate _constructPredicate(Set /* of BasicType */ symmBasicTypes_,
							  Map /* LeafId->IntRange */ sigId2atomRange_) {
	// Construct the symmetry-breaking predicate that sets to FALSE those tuples
	// which we know cannot be in their relations because of the way we allocated
	// atoms to scoped sigs
	SymmetryBreakingPredicate sbp = new SymmetryBreakingPredicate();
	for (Iterator relIter = _astInfo.getRelations().iterator(); relIter.hasNext();) {
	    LeafId relId = (LeafId)relIter.next();
	    RelationType relType = _astInfo.getLeafType(relId);
	    boolean someBasicTypeUsed = false;
	    boolean allBasicTypesUsed = true;
	    for (int i=0; i<relType.numBasicTypes(); i++) {
		boolean thisBasicTypeUsed = symmBasicTypes_.contains(relType.getBasicTypeAt(i));
		someBasicTypeUsed |= thisBasicTypeUsed;
		allBasicTypesUsed &= thisBasicTypeUsed;
	    }
	    ExprRelationInfo relInfo = (ExprRelationInfo)_id2Annotation.get(relId);
	    if (relInfo != null && someBasicTypeUsed) {
		ExprTransl relTransl = _relAlloc.getRelationTransl(relId);
		// loop over tuples of the relation
		for (MultiDimIter tupleIter = new MultiDimIter(relType.getScopes());
		     tupleIter.hasNext();) {
		    int[] tupleInds = (int[])tupleIter.next();
		    // first, determine whether the tuple can be zeroed out because
		    // it cannot be in any of the relInfo.restrictedTo annotations.
		    // each annotation is a cross product of several scoped sigs,
		    // e.g. if relId denotes a relation of type A->A then one annotation
		    // might look like B->E where both B and E are subsignatures of basic type A.
		    boolean tupleIncluded = false;
		    for (Iterator restrToAnnotIter = relInfo.restrictedTo.iterator();
			 !tupleIncluded && restrToAnnotIter.hasNext();) {
			RelAnnotation restrToAnnot = (RelAnnotation)restrToAnnotIter.next();
			// can we find a column such that the basic type of the column
			// is in symmBasicTypes (so that we have allocated a particular range
			// of the basic type's atoms to that column's scoped sig in restrToAnnot)
			// and the column's atom in this tuple is outside the range?
			boolean foundExcludingColumn = false;
			for (int col=0; col<tupleInds.length && !foundExcludingColumn; col++) {
			    IntRange colRange = (IntRange)sigId2atomRange_.get(restrToAnnot.relIdAt(col));
			    foundExcludingColumn |=
				(colRange!=null &&
				 !colRange.contains(tupleInds[col]));
			}
			tupleIncluded |= !foundExcludingColumn;
		    }

		    boolean tupleExcluded = false;
		    if (tupleIncluded && allBasicTypesUsed) {
			// so, we were not able to exclude the tuple based on "restrictedTo" annotations.
			// now let's try to exclude the tuple by finding an "excluded" annotation containing
			// the tuple.
			for (Iterator excludedAnnotIter = relInfo.excluded.iterator();
			     !tupleExcluded && excludedAnnotIter.hasNext();) {
			    RelAnnotation excludedAnnot = (RelAnnotation)excludedAnnotIter.next();
			    boolean allColumnsMatch = true;
			    for (int col=0; col<tupleInds.length && allColumnsMatch; col++) {
				IntRange colRange = (IntRange)sigId2atomRange_.get(excludedAnnot.relIdAt(col));
				allColumnsMatch &=
				    (colRange!=null &&
				     colRange.contains(tupleInds[col]));
			    }
			    tupleExcluded |= allColumnsMatch;
			}
		    }  // if (tupleIncluded)...

		    if (!tupleIncluded || tupleExcluded) {
			if (dbg) {
			    System.out.println("Zeroing out tuple: " + Util.str(tupleInds) +
					       " of " + _astInfo.getLeafRep(relId).nodeString()
					       + " " + _astInfo.getLeafType(relId));
			}
			sbp.conjoin(relTransl.getTupleFormula(tupleInds).not());
		    }
		}  // loop over tuples
	    }  // we have annotations for this relation
	}  // loop over relations, zeroing out some tuples

	return sbp;
    }  // _constructPredicate()

    /**
     * Record the fact that we allocate atoms in the given range to the given scoped sig.
     */
    private void _recordAtomRange(LeafId relId_, int fromAtom_, int toAtom_,
				  Map /* LeafId->IntRange */ sigId2atomRange_) {
	Dbg.chk(!sigId2atomRange_.containsKey(relId_));
	IntRange atomRange = new IntRange(fromAtom_, toAtom_);
	sigId2atomRange_.put(relId_, atomRange);
	if (dbg)
	    System.out.println("Recording atom range: " + atomRange +
			       " for " + _astInfo.getLeafRep(relId_).nodeString());
	_allocateScopedSigAtoms(relId_, sigId2atomRange_);
    }

    /**
     * Allocate atoms to the children of this scoped sig.
     * Precondition: sig_ is already a key in _sigId2atomRange
     * Postcondition: each cihld of sig_ is a key in _sigId2atomRange
     */
    private void _allocateScopedSigAtoms(LeafId sig_, Map /* LeafId->IntRange */ sigId2atomRange_) {
	// first, allocate atom ranges to those children
	// for which explicit scopes have been set.  recall that
	// all scoped sigs extending a given scoped sig are disjoint,
	// so we allocate disjoint ranges of atoms to them.
	RelationType sigRelType = _astInfo.getLeafType(sig_);
	Dbg.chk(sigRelType.numBasicTypes() == 1);
	IntRange sigAtomRange = (IntRange)sigId2atomRange_.get(sig_);
	Dbg.chk(sigAtomRange!=null);
	int highestAllocatedAtom = sigAtomRange.from;
	for (Iterator childIter = _sigsInfo.childSigIds(sig_); childIter.hasNext();) {
	    LeafId childId = (LeafId)childIter.next();
	    Dbg.chk(_sigsInfo.isScopedSig(childId) &&
		    _sigsInfo.parentSigId(childId).equals(sig_));
	    RelationType relType = _astInfo.getLeafType(childId);
	    Dbg.chk(relType.equals(sigRelType));
	    Integer scope = (Integer)_leafId2scope.get(childId);
	    if (scope != null) {
		int childAtomRangeTo = highestAllocatedAtom + scope.intValue();
		Dbg.chk(childAtomRangeTo <= sigAtomRange.to);
		_recordAtomRange(childId, highestAllocatedAtom, childAtomRangeTo, sigId2atomRange_);
		highestAllocatedAtom = childAtomRangeTo;
	    }
	}

	// allocate the remaining atoms in the range to
	// children whose scopes were not explicitly set.
	for (Iterator childIter = _sigsInfo.childSigIds(sig_); childIter.hasNext();) {
	    LeafId childId = (LeafId)childIter.next();
	    RelationType relType = _astInfo.getLeafType(childId);
	    Dbg.chk(relType.equals(sigRelType));
	    Integer scope = (Integer)_leafId2scope.get(childId);
	    if (scope == null) {
		_recordAtomRange(childId, highestAllocatedAtom, sigAtomRange.to, sigId2atomRange_);
	    }
	}
    }   // _allocateScopedSigAtoms()
}  // class SBM_Subscopes

